Nuprl Lemma : fun_exp_compose 11,40

T:Type, n:hf:(TT). (f^n o h) = primrec(n;h;i,gf o g TT 
latex


DefinitionsFalse, A, A  B, i  j , P  Q, tt, (i = j), if b then t else f fi , Y, t  T, primrec(n;b;c), f^n, x:AB(x), f o g, , {T}, SQType(T), ff, P & Q, , P  Q, P  Q
Lemmasge wf, nat properties, nat wf, compose wf, primrec add, int seg wf, le wf, primrec wf, fun exp wf

origin